1 /-
2 Copyright (c) 2019 Kenny Lau. All rights reserved.
3 Released under Apache 2.0 license as described in the file LICENSE.
4 Authors: Kenny Lau
5
6 Ring-theoretic supplement of data.polynomial.
7
8 Main result: Hilbert basis theorem, that if a ring is noetherian then so is its polynomial ring.
9 -/
10
11 import data.polynomial data.mv_polynomial
src └─────────────┘ └────────────────┘
12 import ring_theory.subring
src └─────────────────┘
13 import ring_theory.ideals ring_theory.noetherian
src └────────────────┘ └────────────────────┘
14
15 noncomputable theory
16 local attribute [instance, priority 100] classical.prop_decidable
id └─────┘
src └─────┘
typ └─────┘
17
18 universes u v w
19
20 namespace polynomial
21
22 variables (R : Type u) [comm_ring R]
id └───────┘
src └───────┘
typ └───────┘
23
24 /-- The `R`-submodule of `R[X]` consisting of polynomials of degree ≤ `n`. -/
25 def degree_le (n : with_bot ℕ) : submodule R (polynomial R) :=
26 ⨅ k : ℕ, ⨅ h : ↑k > n, (lcoeff R k).ker
27
28 variable {R}
29
30 theorem mem_degree_le {n : with_bot ℕ} {f : polynomial R} :
31 f ∈ degree_le R n ↔ degree f ≤ n :=
32 by simp only [degree_le, submodule.mem_infi, degree_le_iff_coeff_zero, linear_map.mem_ker]; refl
id └───────┘ └────────────────┘ └──────────────────────┘ └────────────────┘
src └─────────┘└───────┘└┘└────────────────┘└┘└──────────────────────┘└┘└────────────────┘┴ └────
typ └─────────┘└───────┘└┘└────────────────┘└┘└──────────────────────┘└┘└────────────────┘┴ └────
doc └─────────┘└───────┘└┘ └┘ └┘ ┴ └────
txt └─────────┘ └┘ └┘ └┘ ┴ └────
par └─────────┘ └┘ └┘ └┘ ┴ └────
pid ┴└──┘└┘ └┘ └┘ └┘ ┴ └
st └───────────────────────────────────────────────────────────────────────────────────
33
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
34 theorem degree_le_mono {m n : with_bot ℕ} (H : m ≤ n) :
id └──────┘ ┴ ┴ ┴ ┴
src └──────┘ ┴ ┴
typ └──────┘ ┴ ┴ ┴ ┴
35 degree_le R m ≤ degree_le R n :=
id └───────┘ ┴ ┴ ┴ └───────┘ ┴ ┴
src └───────┘ ┴ └───────┘
typ └───────┘ ┴ ┴ ┴ └───────┘ ┴ ┴
doc └───────┘ └───────┘
36 λ f hf, mem_degree_le.2 (le_trans (mem_degree_le.1 hf) H)
id ┴ └┘ └───────────┘┴ └──────┘ └───────────┘┴ └┘ ┴
src └───────────┘┴ └──────┘ └───────────┘┴
typ ┴ └┘ └───────────┘┴ └──────┘ └───────────┘┴ └┘ ┴
37
38 theorem degree_le_eq_span_X_pow {n : ℕ} :
id ┴
src ┴
typ ┴
39 degree_le R n = submodule.span R ↑((finset.range (n+1)).image (λ n, X^n) : finset (polynomial R)) :=
id └───────┘ ┴ ┴ ┴ └────────────┘ ┴ ┴ └──────────┘ ┴┴ └───┘ ┴ ┴┴┴ └────┘ └────────┘ ┴
src └───────┘ ┴ └────────────┘ ┴ └──────────┘ ┴ └───┘ ┴┴ └────┘ └────────┘
typ └───────┘ ┴ ┴ ┴ └────────────┘ ┴ ┴ └──────────┘ ┴┴ └───┘ ┴ ┴┴┴ └────┘ └────────┘ ┴
doc └───────┘ └────────────┘ └──────────┘ └───┘ ┴ └────┘ └────────┘
40 begin
st └─────
41 apply le_antisymm,
id └─────────┘
src └────┘└─────────┘
typ └────┘└─────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ──────────────────┘└─
42 { intros p hp, replace hp := mem_degree_le.1 hp,
id └───────────┘ └┘
src └─────────┘ └────────────┘└───────────┘└─┘
typ └─────────┘ └────────────┘└───────────┘└─┘└┘
doc └─────────┘ └────────────┘ └─┘
txt └─────────┘ └────────────┘ └─┘
par └─────────┘ └────────────┘ └─┘
pid └───┘ └─┘┴└─┘ └─┘
st ───┘└─────────┘└────────────────────────────────┘└─
43 rw [← finsupp.sum_single p, finsupp.sum, submodule.mem_coe],
id └────────────────┘ ┴ └─────────┘ └───────────────┘
src └────┘└────────────────┘┴ └┘└─────────┘└┘└───────────────┘┴
typ └────┘└────────────────┘┴┴└┘└─────────┘└┘└───────────────┘┴
doc └────┘ ┴ └┘└─────────┘└┘ ┴
txt └────┘ ┴ └┘ └┘ ┴
par └────┘ ┴ └┘ └┘ ┴
pid └──┘ ┴ └┘ └┘ ┴
st ─────────────────────────────┘└───────────┘└─────────────────┘└──
44 refine submodule.sum_mem _ (λ k hk, _),
id └───────────────┘
src └─────┘└───────────────┘└─┘ └───────┘
typ └─────┘└───────────────┘└─┘ └───────┘
doc └─────┘ └─┘ └───────┘
txt └─────┘ └─┘ └───────┘
par └─────┘ └─┘ └───────┘
pid ┴ └─┘ └───────┘
st ─────────────────────────────────────────┘└─
45 have := with_bot.coe_le_coe.1 (finset.sup_le_iff.1 hp k hk),
id └─────────────────┘ └───────────────┘ └┘ ┴ └┘
src └──────┘└─────────────────┘└─┘ └───────────────┘└─┘ ┴ ┴ ┴
typ └──────┘└─────────────────┘└─┘ └───────────────┘└─┘└┘┴┴┴└┘┴
doc └──────┘ └─┘ └─┘ ┴ ┴ ┴
txt └──────┘ └─┘ └─┘ ┴ ┴ ┴
par └──────┘ └─┘ └─┘ ┴ ┴ ┴
pid └───┘└─┘ └─┘ └─┘ ┴ ┴ ┴
st ──────────────────────────────────────────────────────────────┘└─
46 rw [single_eq_C_mul_X, C_mul'],
id └───────────────┘ └────┘
src └──┘└───────────────┘└┘└────┘┴
typ └──┘└───────────────┘└┘└────┘┴
doc └──┘ └┘ ┴
txt └──┘ └┘ ┴
par └──┘ └┘ ┴
pid └┘ └┘ ┴
st ────────────────────────┘└──────┘└──
47 refine submodule.smul_mem _ _ (submodule.subset_span $ finset.mem_coe.2 $
id └────────────────┘ └───────────────────┘ └────────────┘
src └─────┘└────────────────┘└───┘ └───────────────────┘┴ ┴└────────────┘└─┘ └
typ └─────┘└────────────────┘└───┘ └───────────────────┘┴ ┴└────────────┘└─┘ └
doc └─────┘ └───┘ ┴ ┴ └─┘ └
txt └─────┘ └───┘ ┴ ┴ └─┘ └
par └─────┘ └───┘ ┴ ┴ └─┘ └
pid ┴ └───┘ ┴ ┴ └─┘ └
st ──────────────────────────────────────────────────────────────────────────────
48 finset.mem_image.2 ⟨_, finset.mem_range.2 (nat.lt_succ_of_le this), rfl⟩) },
id └──────────────┘ └──────────────┘ └───────────────┘ └──┘ └─┘
src ─────┘└──────────────┘└─┘ └─┘└──────────────┘└─┘ └───────────────┘┴ └─┘└─┘└─┘
typ ─────┘└──────────────┘└─┘ └─┘└──────────────┘└─┘ └───────────────┘┴└──┘└─┘└─┘└─┘
doc ─────┘ └─┘ └─┘ └─┘ ┴ └─┘ └─┘
txt ─────┘ └─┘ └─┘ └─┘ ┴ └─┘ └─┘
par ─────┘ └─┘ └─┘ └─┘ ┴ └─┘ └─┘
pid ─────┘ └─┘ └─┘ └─┘ ┴ └─┘ └┘┴
st ───────────────────────────────────────────────────────────────────────────────┘└┘└
49 rw [submodule.span_le, finset.coe_image, set.image_subset_iff],
id └───────────────┘ └──────────────┘ └──────────────────┘
src └──┘└───────────────┘└┘└──────────────┘└┘└──────────────────┘┴
typ └──┘└───────────────┘└┘└──────────────┘└┘└──────────────────┘┴
doc └──┘ └┘ └┘└──────────────────┘┴
txt └──┘ └┘ └┘ ┴
par └──┘ └┘ └┘ ┴
pid └┘ └┘ └┘ ┴
st ──────────────────────┘└────────────────┘└────────────────────┘└──
50 intros k hk, apply mem_degree_le.2,
id └───────────┘
src └─────────┘ └────┘└───────────┘└┘
typ └─────────┘ └────┘└───────────┘└┘
doc └─────────┘ └────┘ └┘
txt └─────────┘ └────┘ └┘
par └─────────┘ └────┘ └┘
pid └───┘ ┴ └┘
st ────────────┘└─────────────────────┘└─
51 apply le_trans (degree_X_pow_le _) (with_bot.coe_le_coe.2 $ nat.le_of_lt_succ $ finset.mem_range.1 hk)
id └──────┘ └─────────────┘ └─────────────────┘ └───────────────┘ └──────────────┘ └┘
src └────┘└──────┘┴ └─────────────┘└──┘ └─────────────────┘└─┘ ┴└───────────────┘┴ ┴└──────────────┘└─┘ └┘
typ └────┘└──────┘┴ └─────────────┘└──┘ └─────────────────┘└─┘ ┴└───────────────┘┴ ┴└──────────────┘└─┘└┘└┘
doc └────┘ ┴ └──┘ └─┘ ┴ ┴ ┴ └─┘ └┘
txt └────┘ ┴ └──┘ └─┘ ┴ ┴ ┴ └─┘ └┘
par └────┘ ┴ └──┘ └─┘ ┴ ┴ ┴ └─┘ └┘
pid ┴ ┴ └──┘ └─┘ ┴ ┴ ┴ └─┘ ┴┴
st ────────────────────────────────────────────────────────────────────────────────────────────────────────┘
52 end
st └─┘
53
54 /-- Given a polynomial, return the polynomial whose coefficients are in
55 the ring closure of the original coefficients. -/
56 def restriction (p : polynomial R) : polynomial (ring.closure (↑p.frange : set R)) :=
id └────────┘ ┴ └────────┘ └──────────┘ ┴┴└─────┘ └─┘ ┴
src └────────┘ └────────┘ └──────────┘ ┴ └─────┘ └─┘
typ └────────┘ ┴ └────────┘ └──────────┘ ┴┴└─────┘ └─┘ ┴
doc └────────┘ └────────┘
57 ⟨p.support, λ i, ⟨p.to_fun i,
id ┴└──────┘ ┴ ┴└─────┘ ┴
src └──────┘ └─────┘
typ ┴└──────┘ ┴ ┴└─────┘ ┴
58 if H : p.to_fun i = 0 then H.symm ▸ is_add_submonoid.zero_mem _
id └┘ ┴└─────┘ ┴ ┴ ┴└───┘ ┴ └───────────────────────┘
src └┘ └─────┘ ┴ └───┘ ┴ └───────────────────────┘
typ └┘ ┴└─────┘ ┴ ┴ ┴└───┘ ┴ └───────────────────────┘
59 else ring.subset_closure $ finsupp.mem_frange.2 ⟨H, i, rfl⟩⟩,
id └─────────────────┘ ┴ └────────────────┘┴ ┴ ┴ └─┘
src └─────────────────┘ ┴ └────────────────┘┴ └─┘
typ └─────────────────┘ ┴ └────────────────┘┴ ┴ ┴ └─┘
60 λ i, finsupp.mem_support_iff.trans (not_iff_not_of_iff ⟨λ H, subtype.eq H, subtype.mk.inj⟩)⟩
id ┴ └─────────────────────┘└────┘ └────────────────┘ ┴ └────────┘ ┴ └────────────┘
src └─────────────────────┘└────┘ └────────────────┘ └────────┘ └────────────┘
typ ┴ └─────────────────────┘└────┘ └────────────────┘ ┴ └────────┘ ┴ └────────────┘
61
62 @[simp] theorem coeff_restriction {p : polynomial R} {n : ℕ} : ↑(coeff (restriction p) n) = coeff p n := rfl
id └────────┘ ┴ ┴ ┴ └───┘ └─────────┘ ┴ ┴ ┴ └───┘ ┴ ┴ └─┘
src └────────┘ ┴ ┴ └───┘ └─────────┘ ┴ └───┘ └─┘
typ └────────┘ ┴ ┴ ┴ └───┘ └─────────┘ ┴ ┴ ┴ └───┘ ┴ ┴ └─┘
doc └──┘ └────────┘ └───┘ └─────────┘ └───┘
63
64 @[simp] theorem coeff_restriction' {p : polynomial R} {n : ℕ} : (coeff (restriction p) n).1 = coeff p n := rfl
id └────────┘ ┴ ┴ └───┘ └─────────┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ └─┘
src └────────┘ ┴ └───┘ └─────────┘ ┴ ┴ └───┘ └─┘
typ └────────┘ ┴ ┴ └───┘ └─────────┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ └─┘
doc └──┘ └────────┘ └───┘ └─────────┘ └───┘
65
66 @[simp] theorem degree_restriction {p : polynomial R} : (restriction p).degree = p.degree := rfl
id └────────┘ ┴ └─────────┘ ┴ └────┘ ┴ ┴└─────┘ └─┘
src └────────┘ └─────────┘ └────┘ ┴ └─────┘ └─┘
typ └────────┘ ┴ └─────────┘ ┴ └────┘ ┴ ┴└─────┘ └─┘
doc └──┘ └────────┘ └─────────┘ └────┘ └─────┘
67
68 @[simp] theorem nat_degree_restriction {p : polynomial R} : (restriction p).nat_degree = p.nat_degree := rfl
id └────────┘ ┴ └─────────┘ ┴ └────────┘ ┴ ┴└─────────┘ └─┘
src └────────┘ └─────────┘ └────────┘ ┴ └─────────┘ └─┘
typ └────────┘ ┴ └─────────┘ ┴ └────────┘ ┴ ┴└─────────┘ └─┘
doc └──┘ └────────┘ └─────────┘ └────────┘ └─────────┘
69
70 @[simp] theorem monic_restriction {p : polynomial R} : monic (restriction p) ↔ monic p :=
id └────────┘ ┴ └───┘ └─────────┘ ┴ ┴ └───┘ ┴
src └────────┘ └───┘ └─────────┘ ┴ └───┘
typ └────────┘ ┴ └───┘ └─────────┘ ┴ ┴ └───┘ ┴
doc └──┘ └────────┘ └───┘ └─────────┘ └───┘
71 ⟨λ H, congr_arg subtype.val H, λ H, subtype.eq H⟩
id ┴ └───────┘ └─────────┘ ┴ ┴ └────────┘ ┴
src └───────┘ └─────────┘ └────────┘
typ ┴ └───────┘ └─────────┘ ┴ ┴ └────────┘ ┴
72
73 @[simp] theorem restriction_zero : restriction (0 : polynomial R) = 0 := rfl
id └─────────┘ └────────┘ ┴ ┴ └─┘
src └─────────┘ └────────┘ ┴ └─┘
typ └─────────┘ └────────┘ ┴ ┴ └─┘
doc └──┘ └─────────┘ └────────┘
74
75 @[simp] theorem restriction_one : restriction (1 : polynomial R) = 1 :=
id └─────────┘ └────────┘ ┴ ┴
src └─────────┘ └────────┘ ┴
typ └─────────┘ └────────┘ ┴ ┴
doc └──┘ └─────────┘ └────────┘
76 ext $ λ i, subtype.eq $ by rw [coeff_restriction', coeff_one, coeff_one]; split_ifs; refl
id └─┘ ┴ └────────┘ └────────────────┘ └───────┘ └───────┘
src └─┘ └────────┘ └──┘└────────────────┘└┘└───────┘└┘└───────┘┴ └───────┘ └────
typ └─┘ ┴ └────────┘ └──┘└────────────────┘└┘└───────┘└┘└───────┘┴ └───────┘ └────
doc └──┘ └┘ └┘ ┴ └───────┘ └────
txt └──┘ └┘ └┘ ┴ └───────┘ └────
par └──┘ └┘ └┘ ┴ └───────┘ └────
pid └┘ └┘ └┘ ┴ └
st └─────────────────────┘└─────────┘└─────────┘┴└─────────────────
77
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
78 variables {S : Type v} [comm_ring S] {f : R → S} {x : S}
id └───────┘
src └───────┘
typ └───────┘
79
80 theorem eval₂_restriction {p : polynomial R} :
id └────────┘ ┴
src └────────┘
typ └────────┘ ┴
doc └────────┘
81 eval₂ f x p = eval₂ (f ∘ subtype.val) x p.restriction :=
id └───┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ └─────────┘ ┴ ┴└──────────┘
src └───┘ ┴ └───┘ ┴ └─────────┘ └──────────┘
typ └───┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ └─────────┘ ┴ ┴└──────────┘
doc └───┘ └───┘ └──────────┘
82 rfl
id └─┘
src └─┘
typ └─┘
83
84 section to_subring
85 variables (p : polynomial R) (T : set R) [is_subring T]
id └────────┘ └─┘ └────────┘
src └────────┘ └─┘ └────────┘
typ └────────┘ └─┘ └────────┘
doc └────────┘ └────────┘
86
87 /-- Given a polynomial `p` and a subring `T` that contains the coefficients of `p`,
88 return the corresponding polynomial whose coefficients are in `T. -/
89 def to_subring (hp : ↑p.frange ⊆ T) : polynomial T :=
id ┴┴└─────┘ ┴ ┴ └────────┘ ┴
src ┴ └─────┘ ┴ └────────┘
typ ┴┴└─────┘ ┴ ┴ └────────┘ ┴
doc └────────┘
90 ⟨p.support, λ i, ⟨p.to_fun i,
id ┴└──────┘ ┴ ┴└─────┘ ┴
src └──────┘ └─────┘
typ ┴└──────┘ ┴ ┴└─────┘ ┴
91 if H : p.to_fun i = 0 then H.symm ▸ is_add_submonoid.zero_mem _
id └┘ ┴└─────┘ ┴ ┴ ┴└───┘ ┴ └───────────────────────┘
src └┘ └─────┘ ┴ └───┘ ┴ └───────────────────────┘
typ └┘ ┴└─────┘ ┴ ┴ ┴└───┘ ┴ └───────────────────────┘
92 else hp $ finsupp.mem_frange.2 ⟨H, i, rfl⟩⟩,
id └┘ ┴ └────────────────┘┴ ┴ ┴ └─┘
src └────────────────┘┴ └─┘
typ └┘ ┴ └────────────────┘┴ ┴ ┴ └─┘
93 λ i, finsupp.mem_support_iff.trans (not_iff_not_of_iff ⟨λ H, subtype.eq H, subtype.mk.inj⟩)⟩
id ┴ └─────────────────────┘└────┘ └────────────────┘ ┴ └────────┘ ┴ └────────────┘
src └─────────────────────┘└────┘ └────────────────┘ └────────┘ └────────────┘
typ ┴ └─────────────────────┘└────┘ └────────────────┘ ┴ └────────┘ ┴ └────────────┘
94
95 variables (hp : ↑p.frange ⊆ T)
id ┴ └─────┘ ┴
src ┴ └─────┘ ┴
typ ┴ └─────┘ ┴
96 include hp
97
98 @[simp] theorem coeff_to_subring {n : ℕ} : ↑(coeff (to_subring p T hp) n) = coeff p n := rfl
id ┴ ┴ └───┘ └────────┘ ┴ ┴ └┘ ┴ ┴ └───┘ ┴ ┴ └─┘
src ┴ ┴ └───┘ └────────┘ ┴ └───┘ └─┘
typ ┴ ┴ └───┘ └────────┘ ┴ ┴ └┘ ┴ ┴ └───┘ ┴ ┴ └─┘
doc └──┘ └───┘ └────────┘ └───┘
99
100 @[simp] theorem coeff_to_subring' {n : ℕ} : (coeff (to_subring p T hp) n).1 = coeff p n := rfl
id ┴ └───┘ └────────┘ ┴ ┴ └┘ ┴ ┴ ┴ └───┘ ┴ ┴ └─┘
src ┴ └───┘ └────────┘ ┴ ┴ └───┘ └─┘
typ ┴ └───┘ └────────┘ ┴ ┴ └┘ ┴ ┴ ┴ └───┘ ┴ ┴ └─┘
doc └──┘ └───┘ └────────┘ └───┘
101
102 @[simp] theorem degree_to_subring : (to_subring p T hp).degree = p.degree := rfl
id └────────┘ ┴ ┴ └┘ └────┘ ┴ ┴└─────┘ └─┘
src └────────┘ └────┘ ┴ └─────┘ └─┘
typ └────────┘ ┴ ┴ └┘ └────┘ ┴ ┴└─────┘ └─┘
doc └──┘ └────────┘ └────┘ └─────┘
103
104 @[simp] theorem nat_degree_to_subring : (to_subring p T hp).nat_degree = p.nat_degree := rfl
id └────────┘ ┴ ┴ └┘ └────────┘ ┴ ┴└─────────┘ └─┘
src └────────┘ └────────┘ ┴ └─────────┘ └─┘
typ └────────┘ ┴ ┴ └┘ └────────┘ ┴ ┴└─────────┘ └─┘
doc └──┘ └────────┘ └────────┘ └─────────┘
105
106 @[simp] theorem monic_to_subring : monic (to_subring p T hp) ↔ monic p :=
id └───┘ └────────┘ ┴ ┴ └┘ ┴ └───┘ ┴
src └───┘ └────────┘ ┴ └───┘
typ └───┘ └────────┘ ┴ ┴ └┘ ┴ └───┘ ┴
doc └──┘ └───┘ └────────┘ └───┘
107 ⟨λ H, congr_arg subtype.val H, λ H, subtype.eq H⟩
id ┴ └───────┘ └─────────┘ ┴ ┴ └────────┘ ┴
src └───────┘ └─────────┘ └────────┘
typ ┴ └───────┘ └─────────┘ ┴ ┴ └────────┘ ┴
108
109 omit hp
110
111 @[simp] theorem to_subring_zero : to_subring (0 : polynomial R) T (set.empty_subset _) = 0 := rfl
id └────────┘ └────────┘ ┴ ┴ └──────────────┘ ┴ └─┘
src └────────┘ └────────┘ └──────────────┘ ┴ └─┘
typ └────────┘ └────────┘ ┴ ┴ └──────────────┘ ┴ └─┘
doc └──┘ └────────┘ └────────┘
112
113 @[simp] theorem to_subring_one : to_subring (1 : polynomial R) T
id └────────┘ └────────┘ ┴ ┴
src └────────┘ └────────┘
typ └────────┘ └────────┘ ┴ ┴
doc └──┘ └────────┘ └────────┘
114 (set.subset.trans (finset.coe_subset.2 finsupp.frange_single)
id └──────────────┘ └───────────────┘┴ └───────────────────┘
src └──────────────┘ └───────────────┘┴ └───────────────────┘
typ └──────────────┘ └───────────────┘┴ └───────────────────┘
115 (set.singleton_subset_iff.2 (is_submonoid.one_mem _))) = 1 :=
id └──────────────────────┘┴ └──────────────────┘ ┴
src └──────────────────────┘┴ └──────────────────┘ ┴
typ └──────────────────────┘┴ └──────────────────┘ ┴
116 ext $ λ i, subtype.eq $ by rw [coeff_to_subring', coeff_one, coeff_one]; split_ifs; refl
id └─┘ ┴ └────────┘ └───────────────┘ └───────┘ └───────┘
src └─┘ └────────┘ └──┘└───────────────┘└┘└───────┘└┘└───────┘┴ └───────┘ └───┘
typ └─┘ ┴ └────────┘ └──┘└───────────────┘└┘└───────┘└┘└───────┘┴ └───────┘ └───┘
doc └──┘ └┘ └┘ ┴ └───────┘ └───┘
txt └──┘ └┘ └┘ ┴ └───────┘ └───┘
par └──┘ └┘ └┘ ┴ └───────┘ └───┘
pid └┘ └┘ └┘ ┴ ┴
st └────────────────────┘└─────────┘└─────────┘┴└────────────────┘
117 end to_subring
118
119 variables (T : set R) [is_subring T]
id └─┘ └────────┘
src └─┘ └────────┘
typ └─┘ └────────┘
doc └────────┘
120
121 /-- Given a polynomial whose coefficients are in some subring, return
122 the corresponding polynomial whose coefificents are in the ambient ring. -/
123 def of_subring (p : polynomial T) : polynomial R :=
id └────────┘ ┴ └────────┘ ┴
src └────────┘ └────────┘
typ └────────┘ ┴ └────────┘ ┴
doc └────────┘ └────────┘
124 ⟨p.support, subtype.val ∘ p.to_fun,
id ┴└──────┘ └─────────┘ ┴ ┴└─────┘
src └──────┘ └─────────┘ ┴ └─────┘
typ ┴└──────┘ └─────────┘ ┴ ┴└─────┘
125 λ n, finsupp.mem_support_iff.trans (not_iff_not_of_iff
id ┴ └─────────────────────┘└────┘ └────────────────┘
src └─────────────────────┘└────┘ └────────────────┘
typ ┴ └─────────────────────┘└────┘ └────────────────┘
126 ⟨λ h, congr_arg subtype.val h, λ h, subtype.eq h⟩)⟩
id ┴ └───────┘ └─────────┘ ┴ ┴ └────────┘ ┴
src └───────┘ └─────────┘ └────────┘
typ ┴ └───────┘ └─────────┘ ┴ ┴ └────────┘ ┴
127
128 @[simp] theorem frange_of_subring {p : polynomial T} :
id └────────┘ ┴
src └────────┘
typ └────────┘ ┴
doc └──┘ └────────┘
129 ↑(p.of_subring T).frange ⊆ T :=
id ┴ ┴└─────────┘ ┴ └────┘ ┴ ┴
src ┴ └─────────┘ └────┘ ┴
typ ┴ ┴└─────────┘ ┴ └────┘ ┴ ┴
doc └─────────┘
130 λ y H, let ⟨hy, x, hx⟩ := finsupp.mem_frange.1 H in hx ▸ (p.to_fun x).2
id ┴ ┴ └─┘ ┴ └┘ └────────────────┘┴ ┴ ┴ ┴└─────┘ ┴
src └────────────────┘┴ ┴ └─────┘ ┴
typ ┴ ┴ └─┘ ┴ └┘ └────────────────┘┴ ┴ ┴ ┴└─────┘ ┴
131
132 end polynomial
133
134 variables {R : Type u} [comm_ring R]
id ┴ └───────┘
src └───────┘
typ ┴ └───────┘
135
136 namespace ideal
137 open polynomial
138
139 /-- Transport an ideal of `R[X]` to an `R`-submodule of `R[X]`. -/
140 def of_polynomial (I : ideal (polynomial R)) : submodule R (polynomial R) :=
id └───┘ └────────┘ ┴ └───────┘ ┴ └────────┘ ┴
src └───┘ └────────┘ └───────┘ └────────┘
typ └───┘ └────────┘ ┴ └───────┘ ┴ └────────┘ ┴
doc └────────┘ └───────┘ └────────┘
141 { carrier := I.carrier,
id ┴└──────┘
src └──────┘
typ ┴└──────┘
142 zero := I.zero_mem,
id ┴└───────┘
src └───────┘
typ ┴└───────┘
143 add := λ _ _, I.add_mem,
id ┴ ┴ ┴└──────┘
src └──────┘
typ ┴ ┴ ┴└──────┘
144 smul := λ c x H, by rw [← C_mul']; exact submodule.smul_mem _ _ H }
id ┴ ┴ ┴ └────┘ └────────────────┘ ┴
src └────┘└────┘┴ └────┘└────────────────┘└───┘ ┴
typ ┴ ┴ ┴ └────┘└────┘┴ └────┘└────────────────┘└───┘┴┴
doc └────┘ ┴ └────┘ └───┘ ┴
txt └────┘ ┴ └────┘ └───┘ ┴
par └────┘ ┴ └────┘ └───┘ ┴
pid └──┘ ┴ ┴ └───┘ ┴
st └───────────┘┴└───────────────────────────────┘
145
146 variables {I : ideal (polynomial R)}
id └───┘ └────────┘
src └───┘ └────────┘
typ └───┘ └────────┘
doc └────────┘
147 theorem mem_of_polynomial (x) : x ∈ I.of_polynomial ↔ x ∈ I := iff.rfl
id ┴ ┴ ┴└────────────┘ ┴ ┴ ┴ ┴ └─────┘
src ┴ └────────────┘ ┴ ┴ └─────┘
typ ┴ ┴ ┴└────────────┘ ┴ ┴ ┴ ┴ └─────┘
doc └────────────┘
148 variables (I)
149
150 /-- Given an ideal `I` of `R[X]`, make the `R`-submodule of `I`
151 consisting of polynomials of degree ≤ `n`. -/
152 def degree_le (n : with_bot ℕ) : submodule R (polynomial R) :=
id └──────┘ ┴ └───────┘ ┴ └────────┘ ┴
src └──────┘ ┴ └───────┘ └────────┘
typ └──────┘ ┴ └───────┘ ┴ └────────┘ ┴
doc └───────┘ └────────┘
153 degree_le R n ⊓ I.of_polynomial
id └───────┘ ┴ ┴ ┴ ┴└────────────┘
src └───────┘ ┴ └────────────┘
typ └───────┘ ┴ ┴ ┴ ┴└────────────┘
doc └───────┘ └────────────┘
154
155 /-- Given an ideal `I` of `R[X]`, make the ideal in `R` of
156 leading coefficients of polynomials in `I` with degree ≤ `n`. -/
157 def leading_coeff_nth (n : ℕ) : ideal R :=
id ┴ └───┘ ┴
src ┴ └───┘
typ ┴ └───┘ ┴
158 (I.degree_le n).map $ lcoeff R n
id ┴└────────┘ ┴ └─┘ └────┘ ┴ ┴
src └────────┘ └─┘ └────┘
typ ┴└────────┘ ┴ └─┘ └────┘ ┴ ┴
doc └────────┘ └─┘
159
160 theorem mem_leading_coeff_nth (n : ℕ) (x) :
id ┴
src ┴
typ ┴
161 x ∈ I.leading_coeff_nth n ↔ ∃ p ∈ I, degree p ≤ n ∧ leading_coeff p = x :=
id ┴ ┴ ┴└────────────────┘ ┴ ┴ ┴ ┴ ┴┴ └────┘ ┴ ┴ ┴ ┴ └───────────┘ ┴ ┴ ┴
src ┴ └────────────────┘ ┴ ┴ ┴ └────┘ ┴ ┴ └───────────┘ ┴
typ ┴ ┴ ┴└────────────────┘ ┴ ┴ ┴ ┴ ┴┴ └────┘ ┴ ┴ ┴ ┴ └───────────┘ ┴ ┴ ┴
doc └────────────────┘ └────┘ └───────────┘
162 begin
st └─────
163 simp only [leading_coeff_nth, degree_le, submodule.mem_map, lcoeff_apply, submodule.mem_inf, mem_degree_le],
id └───────────────┘ └───────┘ └───────────────┘ └──────────┘ └───────────────┘ └───────────┘
src └─────────┘└───────────────┘└┘└───────┘└┘└───────────────┘└┘└──────────┘└┘└───────────────┘└┘└───────────┘┴
typ └─────────┘└───────────────┘└┘└───────┘└┘└───────────────┘└┘└──────────┘└┘└───────────────┘└┘└───────────┘┴
doc └─────────┘└───────────────┘└┘└───────┘└┘ └┘ └┘ └┘ ┴
txt └─────────┘ └┘ └┘ └┘ └┘ └┘ ┴
par └─────────┘ └┘ └┘ └┘ └┘ └┘ ┴
pid ┴└──┘└┘ └┘ └┘ └┘ └┘ └┘ ┴
st ────────────────────────────────────────────────────────────────────────────────────────────────────────────┘└─
164 split,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ──────┘└─
165 { rintro ⟨p, ⟨hpdeg, hpI⟩, rfl⟩,
src └───────────────────────────┘
typ └───────────────────────────┘
doc └───────────────────────────┘
txt └───────────────────────────┘
par └───────────────────────────┘
pid └─────────────────────┘
st ───┘└───────────────────────────┘└─
166 cases lt_or_eq_of_le hpdeg with hpdeg hpdeg,
id └────────────┘ └───┘
src └────┘└────────────┘┴ └───────────────┘
typ └────┘└────────────┘┴└───┘└───────────────┘
doc └────┘ ┴ └───────────────┘
txt └────┘ ┴ └───────────────┘
par └────┘ ┴ └───────────────┘
pid ┴ ┴ └───────────────┘
st ──────────────────────────────────────────────┘└─
167 { refine ⟨0, I.zero_mem, lattice.bot_le, _⟩,
id └────────┘ └────────────┘
src └─────┘ └─┘└────────┘└┘└────────────┘└──┘
typ └─────┘ └─┘└────────┘└┘└────────────┘└──┘
doc └─────┘ └─┘ └┘ └──┘
txt └─────┘ └─┘ └┘ └──┘
par └─────┘ └─┘ └┘ └──┘
pid ┴ └─┘ └┘ └──┘
st ─────┘└───────────────────────────────────────┘└─
168 rw [leading_coeff_zero, eq_comm],
id └────────────────┘ └─────┘
src └──┘└────────────────┘└┘└─────┘┴
typ └──┘└────────────────┘└┘└─────┘┴
doc └──┘ └┘ ┴
txt └──┘ └┘ ┴
par └──┘ └┘ ┴
pid └┘ └┘ ┴
st ───────────────────────────┘└───────┘└──
169 exact coeff_eq_zero_of_degree_lt hpdeg },
id └────────────────────────┘ └───┘
src └────┘└────────────────────────┘┴ ┴
typ └────┘└────────────────────────┘┴└───┘┴
doc └────┘ ┴ ┴
txt └────┘ ┴ ┴
par └────┘ ┴ ┴
pid ┴ ┴ ┴
st ────────────────────────────────────────────┘└┘└
170 { refine ⟨p, hpI, le_of_eq hpdeg, _⟩,
id ┴ └─┘ └──────┘ └───┘
src └─────┘ └┘ └┘└──────┘┴ └──┘
typ └─────┘ ┴└┘└─┘└┘└──────┘┴└───┘└──┘
doc └─────┘ └┘ └┘ ┴ └──┘
txt └─────┘ └┘ └┘ ┴ └──┘
par └─────┘ └┘ └┘ ┴ └──┘
pid ┴ └┘ └┘ ┴ └──┘
st ───────────────────────────────────────┘└─
171 rw [leading_coeff, nat_degree, hpdeg], refl } },
id └───────────┘ └────────┘ └───┘
src └──┘└───────────┘└┘└────────┘└┘ ┴ └───┘
typ └──┘└───────────┘└┘└────────┘└┘└───┘┴ └───┘
doc └──┘└───────────┘└┘└────────┘└┘ ┴ └───┘
txt └──┘ └┘ └┘ ┴ └───┘
par └──┘ └┘ └┘ ┴ └───┘
pid └┘ └┘ └┘ ┴ ┴
st ──────────────────────┘└──────────┘└─────┘└──────┘└──┘└
172 { rintro ⟨p, hpI, hpdeg, rfl⟩,
src └─────────────────────────┘
typ └─────────────────────────┘
doc └─────────────────────────┘
txt └─────────────────────────┘
par └─────────────────────────┘
pid └───────────────────┘
st ──────────────────────────────┘└─
173 have : nat_degree p + (n - nat_degree p) = n,
id ┴ ┴ └────────┘ ┴ ┴ ┴
src └─────┘ ┴ ┴┴┴ ┴┴┴└────────┘┴ └┘┴┴
typ └─────┘ ┴ ┴┴┴ ┴┴┴└────────┘┴┴└┘┴┴┴
doc └─────┘ ┴ ┴ ┴ ┴ ┴└────────┘┴ └┘ ┴
txt └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴
par └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴
pid └───┘└┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴
st ───────────────────────────────────────────────┘└─
174 { exact nat.add_sub_cancel' (nat_degree_le_of_degree_le hpdeg) },
id └─────────────────┘ └────────────────────────┘ └───┘
src └────┘└─────────────────┘┴ └────────────────────────┘┴ └┘
typ └────┘└─────────────────┘┴ └────────────────────────┘┴└───┘└┘
doc └────┘ ┴ ┴ └┘
txt └────┘ ┴ ┴ └┘
par └────┘ ┴ ┴ └┘
pid ┴ ┴ ┴ ┴┴
st ─────┘└───────────────────────────────────────────────────────────┘└┘└
175 refine ⟨p * X ^ (n - nat_degree p), ⟨_, I.mul_mem_right hpI⟩, _⟩,
id ┴ ┴ ┴ ┴ └────────┘ ┴ └─────────────┘ └─┘
src └─────┘ ┴┴┴┴┴┴┴ ┴ ┴└────────┘┴ └─┘ └─┘└─────────────┘┴ └───┘
typ └─────┘ ┴┴┴┴┴┴┴ ┴┴ ┴└────────┘┴┴└─┘ └─┘└─────────────┘┴└─┘└───┘
doc └─────┘ ┴ ┴┴┴ ┴ ┴ ┴└────────┘┴ └─┘ └─┘ ┴ └───┘
txt └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └─┘ ┴ └───┘
par └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └─┘ ┴ └───┘
pid ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └─┘ ┴ └───┘
st ───────────────────────────────────────────────────────────────────┘└─
176 { apply le_trans (degree_mul_le _ _) _,
id └──────┘ └───────────┘
src └────┘└──────┘┴ └───────────┘└─────┘
typ └────┘└──────┘┴ └───────────┘└─────┘
doc └────┘ ┴ └─────┘
txt └────┘ ┴ └─────┘
par └────┘ ┴ └─────┘
pid ┴ ┴ └─────┘
st ─────┘└──────────────────────────────────┘└─
177 apply le_trans (add_le_add' (degree_le_nat_degree) (degree_X_pow_le _)) _,
id └──────┘ └─────────┘ └──────────────────┘ └─────────────┘
src └────┘└──────┘┴ └─────────┘┴ └──────────────────┘└┘ └─────────────┘└────┘
typ └────┘└──────┘┴ └─────────┘┴ └──────────────────┘└┘ └─────────────┘└────┘
doc └────┘ ┴ ┴ └┘ └────┘
txt └────┘ ┴ ┴ └┘ └────┘
par └────┘ ┴ ┴ └┘ └────┘
pid ┴ ┴ ┴ └┘ └────┘
st ──────────────────────────────────────────────────────────────────────────────┘└─
178 rw [← with_bot.coe_add, this],
id └──────────────┘ └──┘
src └────┘└──────────────┘└┘ ┴
typ └────┘└──────────────┘└┘└──┘┴
doc └────┘ └┘ ┴
txt └────┘ └┘ ┴
par └────┘ └┘ ┴
pid └──┘ └┘ ┴
st ───────────────────────────┘└────┘└──
179 exact le_refl _ },
id └─────┘
src └────┘└─────┘└─┘
typ └────┘└─────┘└─┘
doc └────┘ └─┘
txt └────┘ └─┘
par └────┘ └─┘
pid ┴ └┘┴
st ─────────────────────┘└┘└
180 { rw [leading_coeff, ← coeff_mul_X_pow p (n - nat_degree p), this] } }
id └───────────┘ └─────────────┘ ┴ └────────┘ ┴ └──┘
src └──┘└───────────┘└──┘└─────────────┘┴ ┴ ┴ ┴└────────┘┴ └─┘ └┘
typ └──┘└───────────┘└──┘└─────────────┘┴ ┴ ┴┴ ┴└────────┘┴┴└─┘└──┘└┘
doc └──┘└───────────┘└──┘ ┴ ┴ ┴ ┴└────────┘┴ └─┘ └┘
txt └──┘ └──┘ ┴ ┴ ┴ ┴ ┴ └─┘ └┘
par └──┘ └──┘ ┴ ┴ ┴ ┴ ┴ └─┘ └┘
pid └┘ └──┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴┴
st ──────────────────────┘└──────────────────────────────────────┘└────┘┴┴└───
181 end
st ──┘
182
183 theorem mem_leading_coeff_nth_zero (x) :
184 x ∈ I.leading_coeff_nth 0 ↔ C x ∈ I :=
id ┴ ┴ ┴└────────────────┘ ┴ ┴ ┴ ┴ ┴
src ┴ └────────────────┘ ┴ ┴ ┴
typ ┴ ┴ ┴└────────────────┘ ┴ ┴ ┴ ┴ ┴
doc └────────────────┘ ┴
185 (mem_leading_coeff_nth _ _ _).trans
id └───────────────────┘ └───┘
src └───────────────────┘ └───┘
typ └───────────────────┘ └───┘
186 ⟨λ ⟨p, hpI, hpdeg, hpx⟩, by rwa [← hpx, leading_coeff,
id ┴ └─┘ └───────────┘
src └─────┘ └┘└───────────┘└─
typ ┴ └─────┘└─┘└┘└───────────┘└─
doc └─────┘ └┘└───────────┘└─
txt └─────┘ └┘ └─
par └─────┘ └┘ └─
pid └──┘ └┘ └─
st └─────────┘└─────────────┘└─
187 nat.eq_zero_of_le_zero (nat_degree_le_of_degree_le hpdeg),
id └────────────────────┘ └────────────────────────┘ └───┘
src ─┘└────────────────────┘┴ └────────────────────────┘┴ └──
typ ─┘└────────────────────┘┴ └────────────────────────┘┴└───┘└──
doc ─┘ ┴ ┴ └──
txt ─┘ ┴ ┴ └──
par ─┘ ┴ ┴ └──
pid ─┘ ┴ ┴ └──
st ──────────────────────────────────────────────────────────┘└─
188 ← eq_C_of_degree_le_zero hpdeg],
id └────────────────────┘ └───┘
src ───┘└────────────────────┘┴ ┴
typ ───┘└────────────────────┘┴└───┘┴
doc ───┘ ┴ ┴
txt ───┘ ┴ ┴
par ───┘ ┴ ┴
pid ───┘ ┴ ┴
st ───────────────────────────────┘┴
189 λ hx, ⟨C x, hx, degree_C_le, leading_coeff_C x⟩⟩
id └┘ ┴ ┴ └┘ └─────────┘ └─────────────┘ ┴
src ┴ └─────────┘ └─────────────┘
typ └┘ ┴ ┴ └┘ └─────────┘ └─────────────┘ ┴
doc ┴
190
191 theorem leading_coeff_nth_mono {m n : ℕ} (H : m ≤ n) :
id ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴
192 I.leading_coeff_nth m ≤ I.leading_coeff_nth n :=
id ┴└────────────────┘ ┴ ┴ ┴└────────────────┘ ┴
src └────────────────┘ ┴ └────────────────┘
typ ┴└────────────────┘ ┴ ┴ ┴└────────────────┘ ┴
doc └────────────────┘ └────────────────┘
193 begin
st └─────
194 intros r hr,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └───┘
st ────────────┘└─
195 simp only [submodule.mem_coe, mem_leading_coeff_nth] at hr ⊢,
id └───────────────┘ └───────────────────┘
src └─────────┘└───────────────┘└┘└───────────────────┘└───────┘
typ └─────────┘└───────────────┘└┘└───────────────────┘└───────┘
doc └─────────┘ └┘ └───────┘
txt └─────────┘ └┘ └───────┘
par └─────────┘ └┘ └───────┘
pid ┴└──┘└┘ └┘ ┴┴└─────┘
st ─────────────────────────────────────────────────────────────┘└─
196 rcases hr with ⟨p, hpI, hpdeg, rfl⟩,
id └┘
src └─────┘ └────────────────────────┘
typ └─────┘└┘└────────────────────────┘
doc └─────┘ └────────────────────────┘
txt └─────┘ └────────────────────────┘
par └─────┘ └────────────────────────┘
pid ┴ └────────────────────────┘
st ────────────────────────────────────┘└─
197 refine ⟨p * X ^ (n - m), I.mul_mem_right hpI, _, leading_coeff_mul_X_pow⟩,
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────────────┘ └─┘ └─────────────────────┘
src └─────┘ ┴┴┴┴┴┴┴ ┴┴┴ └─┘└─────────────┘┴ └───┘└─────────────────────┘┴
typ └─────┘ ┴┴┴┴┴┴┴┴ ┴┴┴┴┴└─┘└─────────────┘┴└─┘└───┘└─────────────────────┘┴
doc └─────┘ ┴ ┴┴┴ ┴ ┴ ┴ └─┘ ┴ └───┘ ┴
txt └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ └───┘ ┴
par └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ └───┘ ┴
pid ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ └───┘ ┴
st ──────────────────────────────────────────────────────────────────────────┘└─
198 refine le_trans (degree_mul_le _ _) _,
id └──────┘ └───────────┘
src └─────┘└──────┘┴ └───────────┘└─────┘
typ └─────┘└──────┘┴ └───────────┘└─────┘
doc └─────┘ ┴ └─────┘
txt └─────┘ ┴ └─────┘
par └─────┘ ┴ └─────┘
pid ┴ ┴ └─────┘
st ──────────────────────────────────────┘└─
199 refine le_trans (add_le_add' hpdeg (degree_X_pow_le _)) _,
id └──────┘ └─────────┘ └───┘ └─────────────┘
src └─────┘└──────┘┴ └─────────┘┴ ┴ └─────────────┘└────┘
typ └─────┘└──────┘┴ └─────────┘┴└───┘┴ └─────────────┘└────┘
doc └─────┘ ┴ ┴ ┴ └────┘
txt └─────┘ ┴ ┴ ┴ └────┘
par └─────┘ ┴ ┴ ┴ └────┘
pid ┴ ┴ ┴ ┴ └────┘
st ──────────────────────────────────────────────────────────┘└─
200 rw [← with_bot.coe_add, nat.add_sub_cancel' H],
id └──────────────┘ └─────────────────┘ ┴
src └────┘└──────────────┘└┘└─────────────────┘┴ ┴
typ └────┘└──────────────┘└┘└─────────────────┘┴┴┴
doc └────┘ └┘ ┴ ┴
txt └────┘ └┘ ┴ ┴
par └────┘ └┘ ┴ ┴
pid └──┘ └┘ ┴ ┴
st ───────────────────────┘└─────────────────────┘└──
201 exact le_refl _
id └─────┘
src └────┘└─────┘└─┘
typ └────┘└─────┘└─┘
doc └────┘ └─┘
txt └────┘ └─┘
par └────┘ └─┘
pid ┴ └┘┴
st ─────────────────┘
202 end
st └─┘
203
204 /-- Given an ideal `I` in `R[X]`, make the ideal in `R` of the
205 leading coefficients in `I`. -/
206 def leading_coeff : ideal R :=
id └───┘ ┴
src └───┘
typ └───┘ ┴
207 ⨆ n : ℕ, I.leading_coeff_nth n
id ┴ ┴┴ ┴└────────────────┘ ┴
src ┴ ┴┴ └────────────────┘
typ ┴ ┴┴ ┴└────────────────┘ ┴
doc ┴ ┴ └────────────────┘
208
209 theorem mem_leading_coeff (x) :
210 x ∈ I.leading_coeff ↔ ∃ p ∈ I, polynomial.leading_coeff p = x :=
id ┴ ┴ ┴└────────────┘ ┴ ┴ ┴ ┴┴ └──────────────────────┘ ┴ ┴ ┴
src ┴ └────────────┘ ┴ ┴ ┴ └──────────────────────┘ ┴
typ ┴ ┴ ┴└────────────┘ ┴ ┴ ┴ ┴┴ └──────────────────────┘ ┴ ┴ ┴
doc └────────────┘ └──────────────────────┘
211 begin
st └─────
212 rw [leading_coeff, submodule.mem_supr_of_directed],
id └───────────┘ └────────────────────────────┘
src └──┘└───────────┘└┘└────────────────────────────┘┴
typ └──┘└───────────┘└┘└────────────────────────────┘┴
doc └──┘└───────────┘└┘ ┴
txt └──┘ └┘ ┴
par └──┘ └┘ ┴
pid └┘ └┘ ┴
st ──────────────────┘└──────────────────────────────┘└──
213 simp only [mem_leading_coeff_nth],
id └───────────────────┘
src └─────────┘└───────────────────┘┴
typ └─────────┘└───────────────────┘┴
doc └─────────┘ ┴
txt └─────────┘ ┴
par └─────────┘ ┴
pid ┴└──┘└┘ ┴
st ──────────────────────────────────┘└─
214 { split, { rintro ⟨i, p, hpI, hpdeg, rfl⟩, exact ⟨p, hpI, rfl⟩ },
id ┴ └─┘ └─┘
src └───┘ └────────────────────────────┘ └────┘ └┘ └┘└─┘└┘
typ └───┘ └────────────────────────────┘ └────┘ ┴└┘└─┘└┘└─┘└┘
doc └───┘ └────────────────────────────┘ └────┘ └┘ └┘ └┘
txt └───┘ └────────────────────────────┘ └────┘ └┘ └┘ └┘
par └───┘ └────────────────────────────┘ └────┘ └┘ └┘ └┘
pid └──────────────────────┘ ┴ └┘ └┘ ┴┴
st ───┘└───┘└──┘└────────────────────────────┘└────────────────────┘└┘└
215 rintro ⟨p, hpI, rfl⟩, exact ⟨nat_degree p, p, hpI, degree_le_nat_degree, rfl⟩ },
id └────────┘ ┴ └─┘ └──────────────────┘ └─┘
src └──────────────────┘ └────┘ └────────┘┴ └┘ └┘ └┘└──────────────────┘└┘└─┘└┘
typ └──────────────────┘ └────┘ └────────┘┴ └┘┴└┘└─┘└┘└──────────────────┘└┘└─┘└┘
doc └──────────────────┘ └────┘ └────────┘┴ └┘ └┘ └┘ └┘ └┘
txt └──────────────────┘ └────┘ ┴ └┘ └┘ └┘ └┘ └┘
par └──────────────────┘ └────┘ ┴ └┘ └┘ └┘ └┘ └┘
pid └────────────┘ ┴ ┴ └┘ └┘ └┘ └┘ ┴┴
st ───────────────────────┘└────────────────────────────────────────────────────────┘└┘└
216 { exact ⟨0⟩ },
src └────┘ └─┘
typ └────┘ └─┘
doc └────┘ └─┘
txt └────┘ └─┘
par └────┘ └─┘
pid ┴ └┘┴
st ───┘└────────┘└┘└
217 intros i j, exact ⟨i + j, I.leading_coeff_nth_mono (nat.le_add_right _ _),
id ┴ ┴ ┴ └──────────────┘
src └────────┘ └────┘ ┴┴┴ └┘ ┴ └──────────────┘└──────
typ └────────┘ └────┘ ┴┴┴┴┴└┘ ┴ └──────────────┘└──────
doc └────────┘ └────┘ ┴ ┴ └┘ ┴ └──────
txt └────────┘ └────┘ ┴ ┴ └┘ ┴ └──────
par └────────┘ └────┘ ┴ ┴ └┘ ┴ └──────
pid └──┘ ┴ ┴ ┴ └┘ ┴ └──────
st ───────────┘└────────────────────────────────────────────────────────────────
218 I.leading_coeff_nth_mono (nat.le_add_left _ _)⟩
id └──────────────────────┘ └─────────────┘
src ───┘└──────────────────────┘┴ └─────────────┘└─────┘
typ ───┘└──────────────────────┘┴ └─────────────┘└─────┘
doc ───┘ ┴ └─────┘
txt ───┘ ┴ └─────┘
par ───┘ ┴ └─────┘
pid ───┘ ┴ └────┘┴
st ───────────────────────────────────────────────────┘
219 end
st └─┘
220
221 theorem is_fg_degree_le [is_noetherian_ring R] (n : ℕ) :
id └────────────────┘ ┴ ┴
src └────────────────┘ ┴
typ └────────────────┘ ┴ ┴
222 submodule.fg (I.degree_le n) :=
id └──────────┘ ┴└────────┘ ┴
src └──────────┘ └────────┘
typ └──────────┘ ┴└────────┘ ┴
doc └────────┘
223 is_noetherian_submodule_left.1 (is_noetherian_of_fg_of_noetherian _
id └──────────────────────────┘┴ └───────────────────────────────┘
src └──────────────────────────┘┴ └───────────────────────────────┘
typ └──────────────────────────┘┴ └───────────────────────────────┘
224 ⟨_, degree_le_eq_span_X_pow.symm⟩) _
id └─────────────────────┘└───┘
src └─────────────────────┘└───┘
typ └─────────────────────┘└───┘
225
226 end ideal
227
228 /-- Hilbert basis theorem. -/
229 theorem is_noetherian_ring_polynomial [is_noetherian_ring R] : is_noetherian_ring (polynomial R) :=
id └────────────────┘ ┴ └────────────────┘ └────────┘ ┴
src └────────────────┘ └────────────────┘ └────────┘
typ └────────────────┘ ┴ └────────────────┘ └────────┘ ┴
doc └────────┘
230 ⟨assume I : ideal (polynomial R),
id └───┘ └────────┘ ┴
src └───┘ └────────┘
typ └───┘ └────────┘ ┴
doc └────────┘
231 let L := I.leading_coeff in
id ┴ ┴└────────────┘
src └────────────┘
typ ┴ ┴└────────────┘
doc └────────────┘
232 let M := well_founded.min (is_noetherian_iff_well_founded.1 (by apply_instance))
id ┴ └──────────────┘ └────────────────────────────┘┴
src └──────────────┘ └────────────────────────────┘┴ └────────────┘
typ ┴ └──────────────┘ └────────────────────────────┘┴ └────────────┘
doc └──────────────┘ └────────────┘
txt └────────────┘
par └────────────┘
st └─────────────┘
233 (set.range I.leading_coeff_nth) ⟨_, ⟨0, rfl⟩⟩ in
id └───────┘ ┴└────────────────┘ └─┘
src └───────┘ └────────────────┘ └─┘
typ └───────┘ ┴└────────────────┘ └─┘
doc └───────┘ └────────────────┘
234 have hm : M ∈ set.range I.leading_coeff_nth := well_founded.min_mem _ _ _,
id ┴ ┴ └───────┘ ┴└────────────────┘ └──────────────────┘
src ┴ └───────┘ └────────────────┘ └──────────────────┘
typ ┴ ┴ └───────┘ ┴└────────────────┘ └──────────────────┘
doc └───────┘ └────────────────┘
235 let ⟨N, HN⟩ := hm, ⟨s, hs⟩ := I.is_fg_degree_le N in
id └─┘ ┴ └┘ └┘ ┴ └┘ ┴└──────────────┘
src └──────────────┘
typ └─┘ ┴ └┘ └┘ ┴ └┘ ┴└──────────────┘
236 have hm2 : ∀ k, I.leading_coeff_nth k ≤ M := λ k, or.cases_on (le_or_lt k N)
id ┴ ┴└────────────────┘ ┴ ┴ ┴ ┴ └─────────┘ └──────┘ ┴
src └────────────────┘ ┴ └─────────┘ └──────┘
typ ┴ ┴└────────────────┘ ┴ ┴ ┴ ┴ └─────────┘ └──────┘ ┴
doc └────────────────┘
237 (λ h, HN ▸ I.leading_coeff_nth_mono h)
id ┴ ┴ ┴└─────────────────────┘ ┴
src ┴ └─────────────────────┘
typ ┴ ┴ ┴└─────────────────────┘ ┴
238 (λ h x hx, classical.by_contradiction $ λ hxm,
id ┴ ┴ └┘ └────────────────────────┘ └─┘
src └────────────────────────┘
typ ┴ ┴ └┘ └────────────────────────┘ └─┘
239 have ¬M < I.leading_coeff_nth k, by refine well_founded.not_lt_min
id ┴┴ ┴ ┴└────────────────┘ ┴ └─────────────────────┘
src ┴ ┴ └────────────────┘ └─────┘└─────────────────────┘└
typ ┴┴ ┴ ┴└────────────────┘ ┴ └─────┘└─────────────────────┘└
doc └────────────────┘ └─────┘ └
txt └─────┘ └
par └─────┘ └
pid ┴ └
st └───────────────────────────────
240 (well_founded_submodule_gt _ _) _ _ _; exact ⟨k, rfl⟩,
id └───────────────────────┘ ┴ └─┘
src ─────┘ └───────────────────────┘└─────────┘ └────┘ └┘└─┘┴
typ ─────┘ └───────────────────────┘└─────────┘ └────┘ ┴└┘└─┘┴
doc ─────┘ └─────────┘ └────┘ └┘ ┴
txt ─────┘ └─────────┘ └────┘ └┘ ┴
par ─────┘ └─────────┘ └────┘ └┘ ┴
pid ─────┘ └─────────┘ ┴ └┘ ┴
st ──────────────────────────────────────────────────────────┘
241 this ⟨HN ▸ I.leading_coeff_nth_mono (le_of_lt h), λ H, hxm (H hx)⟩),
id └──┘ ┴ ┴└─────────────────────┘ └──────┘ ┴ ┴ └─┘ ┴ └┘
src ┴ └─────────────────────┘ └──────┘
typ └──┘ ┴ ┴└─────────────────────┘ └──────┘ ┴ ┴ └─┘ ┴ └┘
242 have hs2 : ∀ {x}, x ∈ I.degree_le N → x ∈ ideal.span (↑s : set (polynomial R)),
id ┴ ┴ ┴ ┴└────────┘ ┴ ┴ └────────┘ ┴ └─┘ └────────┘ ┴
src ┴ └────────┘ ┴ └────────┘ ┴ └─┘ └────────┘
typ ┴ ┴ ┴ ┴└────────┘ ┴ ┴ └────────┘ ┴ └─┘ └────────┘ ┴
doc └────────┘ └────────┘
243 from hs ▸ λ x hx, submodule.span_induction hx (λ _ hx, ideal.subset_span hx) (ideal.zero_mem _)
id ┴ ┴ └┘ └──────────────────────┘ └┘ ┴ └┘ └───────────────┘ └┘ └────────────┘
src ┴ └──────────────────────┘ └───────────────┘ └────────────┘
typ ┴ ┴ └┘ └──────────────────────┘ └┘ ┴ └┘ └───────────────┘ └┘ └────────────┘
doc └──────────────────────┘
244 (λ _ _, ideal.add_mem _) (λ c f hf, f.C_mul' c ▸ ideal.mul_mem_left _ hf),
id ┴ ┴ └───────────┘ ┴ ┴ └┘ ┴└─────┘ ┴ ┴ └────────────────┘ └┘
src └───────────┘ └─────┘ ┴ └────────────────┘
typ ┴ ┴ └───────────┘ ┴ ┴ └┘ ┴└─────┘ ┴ ┴ └────────────────┘ └┘
245 ⟨s, le_antisymm (ideal.span_le.2 $ λ x hx, have x ∈ I.degree_le N, from hs ▸ submodule.subset_span hx, this.2) $ begin
id └─────────┘ └───────────┘┴ ┴ └┘ ┴ ┴ ┴└────────┘ ┴ └───────────────────┘ └┘ └──┘┴
src └─────────┘ └───────────┘┴ ┴ └────────┘ ┴ └───────────────────┘ ┴
typ └─────────┘ └───────────┘┴ ┴ └┘ ┴ ┴ ┴└────────┘ ┴ └───────────────────┘ └┘ └──┘┴
doc └────────┘
st └─────
246 change I ≤ ideal.span ↑s,
id ┴ ┴ └────────┘ ┴┴
src └─────┘ ┴┴┴└────────┘┴┴
typ └─────┘┴┴┴┴└────────┘┴┴┴
doc └─────┘ ┴ ┴ ┴
txt └─────┘ ┴ ┴ ┴
par └─────┘ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴
st ─────────────────────────┘└─
247 intros p hp, generalize hn : p.nat_degree = k,
id └──────────┘
src └─────────┘ └──────────────┘└──────────┘┴ ┴
typ └─────────┘ └──────────────┘└──────────┘┴ ┴
doc └─────────┘ └──────────────┘└──────────┘┴ ┴
txt └─────────┘ └──────────────┘ ┴ ┴
par └─────────┘ └──────────────┘ ┴ ┴
pid └───┘ └─┘└┘┴ ┴ ┴
st ────────────┘└────────────────────────────────┘└─
248 induction k using nat.strong_induction_on with k ih generalizing p,
id ┴
src └────────┘ └─────────────────────────────────────────────────────┘
typ └────────┘┴└─────────────────────────────────────────────────────┘
doc └────────┘ └─────────────────────────────────────────────────────┘
txt └────────┘ └─────────────────────────────────────────────────────┘
par └────────┘ └─────────────────────────────────────────────────────┘
pid ┴ └────────────────────────────┘└────────┘└─────────────┘
st ───────────────────────────────────────────────────────────────────┘└─
249 cases le_or_lt k N,
id └──────┘ ┴ ┴
src └────┘└──────┘┴ ┴
typ └────┘└──────┘┴┴┴┴
doc └────┘ ┴ ┴
txt └────┘ ┴ ┴
par └────┘ ┴ ┴
pid ┴ ┴ ┴
st ───────────────────┘└─
250 { subst k, refine hs2 ⟨polynomial.mem_degree_le.2
id ┴ └─┘ └──────────────────────┘
src └────┘ └─────┘ ┴ └──────────────────────┘└──
typ └────┘┴ └─────┘└─┘┴ └──────────────────────┘└──
doc └────┘ └─────┘ ┴ └──
txt └────┘ └─────┘ ┴ └──
par └────┘ └─────┘ ┴ └──
pid ┴ ┴ ┴ └──
st ───┘└─────┘└────────────────────────────────────────
251 (le_trans polynomial.degree_le_nat_degree $ with_bot.coe_le_coe.2 h), hp⟩ },
id └──────┘ └─────────────────────────────┘ └─────────────────┘ ┴ └┘
src ─────┘ └──────┘┴└─────────────────────────────┘┴ ┴└─────────────────┘└─┘ └─┘ └┘
typ ─────┘ └──────┘┴└─────────────────────────────┘┴ ┴└─────────────────┘└─┘┴└─┘└┘└┘
doc ─────┘ ┴ ┴ ┴ └─┘ └─┘ └┘
txt ─────┘ ┴ ┴ ┴ └─┘ └─┘ └┘
par ─────┘ ┴ ┴ ┴ └─┘ └─┘ └┘
pid ─────┘ ┴ ┴ ┴ └─┘ └─┘ ┴┴
st ───────────────────────────────────────────────────────────────────────────────┘└┘└
252 { have hp0 : p ≠ 0,
id ┴ ┴
src └─────────┘ ┴┴└┘
typ └─────────┘┴┴┴└┘
doc └─────────┘ ┴ └┘
txt └─────────┘ ┴ └┘
par └─────────┘ ┴ └┘
pid └──────┘└─┘ ┴ ┴┴
st ───────────────────┘└─
253 { rintro rfl, cases hn, exact nat.not_lt_zero _ h },
id └┘ └─────────────┘ ┴
src └────────┘ └────┘ └────┘└─────────────┘└─┘ ┴
typ └────────┘ └────┘└┘ └────┘└─────────────┘└─┘┴┴
doc └────────┘ └────┘ └────┘ └─┘ ┴
txt └────────┘ └────┘ └────┘ └─┘ ┴
par └────────┘ └────┘ └────┘ └─┘ ┴
pid └──┘ ┴ ┴ └─┘ ┴
st ─────┘└────────┘└────────┘└──────────────────────────┘└┘└
254 have : (0 : R) ≠ 1,
id ┴
src └─────┘ └──┘ └┘ └┘
typ └─────┘ └──┘┴└┘ └┘
doc └─────┘ └──┘ └┘ └┘
txt └─────┘ └──┘ └┘ └┘
par └─────┘ └──┘ └┘ └┘
pid └───┘└┘ └──┘ └┘ ┴┴
st ─────────────────────┘└─
255 { intro h, apply hp0, ext i, refine (mul_one _).symm.trans _,
id └─────┘
src └─────┘ └────┘ └───┘ └─────┘ └─────┘└──────────────┘
typ └─────┘ └────┘ └───┘ └─────┘ └─────┘└──────────────┘
doc └─────┘ └────┘ └───┘ └─────┘ └──────────────┘
txt └─────┘ └────┘ └───┘ └─────┘ └──────────────┘
par └─────┘ └────┘ └───┘ └─────┘ └──────────────┘
pid └┘ ┴ └┘ ┴ └──────────────┘
st ─────┘└─────┘└─────────┘└─────┘└───────────────────────────────┘└─
256 rw [← h, mul_zero], refl },
id ┴ └──────┘
src └────┘ └┘└──────┘┴ └───┘
typ └────┘┴└┘└──────┘┴ └───┘
doc └────┘ └┘ ┴ └───┘
txt └────┘ └┘ ┴ └───┘
par └────┘ └┘ ┴ └───┘
pid └──┘ └┘ ┴ ┴
st ────────────┘└────────┘└──────┘└┘└
257 letI : nonzero_comm_ring R := { zero_ne_one := this,
id └───────────────┘ ┴ └──┘
src └─────┘└───────────────┘┴ └──┘ └──────────────┘ └─
typ └─────┘└───────────────┘┴┴└──┘ └──────────────┘└──┘└─
doc └─────┘└───────────────┘┴ └──┘ └──────────────┘ └─
txt └─────┘ ┴ └──┘ └──────────────┘ └─
par └─────┘ ┴ └──┘ └──────────────┘ └─
pid ┴└┘ ┴ └──┘ └──────────────┘ └─
st ─────────────────────────────────────────────────────────
258 ..(infer_instance : comm_ring R) },
id └────────────┘ └───────┘ ┴
src ───────┘ └────────────┘└─┘└───────┘┴ └─┘
typ ───────┘ └────────────┘└─┘└───────┘┴┴└─┘
doc ───────┘ └────────────┘└─┘ ┴ └─┘
txt ───────┘ └─┘ ┴ └─┘
par ───────┘ └─┘ ┴ └─┘
pid ───────┘ └─┘ ┴ └─┘
st ───────────────────────────────────────┘└─
259 have : p.leading_coeff ∈ I.leading_coeff_nth N,
id └─────────────┘ ┴ └─────────────────┘ ┴
src └─────┘└─────────────┘┴┴┴└─────────────────┘┴
typ └─────┘└─────────────┘┴┴┴└─────────────────┘┴┴
doc └─────┘└─────────────┘┴ ┴└─────────────────┘┴
txt └─────┘ ┴ ┴ ┴
par └─────┘ ┴ ┴ ┴
pid └───┘└┘ ┴ ┴ ┴
st ─────────────────────────────────────────────────┘└─
260 { rw HN, exact hm2 k ((I.mem_leading_coeff_nth _ _).2
id └┘ └─┘ ┴ └─────────────────────┘
src └─┘ └────┘ ┴ ┴ └─────────────────────┘└───────
typ └─┘└┘ └────┘└─┘┴┴┴ └─────────────────────┘└───────
doc └─┘ └────┘ ┴ ┴ └───────
txt └─┘ └────┘ ┴ ┴ └───────
par └─┘ └────┘ ┴ ┴ └───────
pid ┴ ┴ ┴ ┴ └───────
st ─────┘└───┘└──────────────────────────────────────────────
261 ⟨_, hp, hn ▸ polynomial.degree_le_nat_degree, rfl⟩) },
id └┘ └┘ ┴ └─────────────────────────────┘ └─┘
src ───────┘ └─┘ └┘ ┴┴┴└─────────────────────────────┘└┘└─┘└─┘
typ ───────┘ └─┘└┘└┘└┘┴┴┴└─────────────────────────────┘└┘└─┘└─┘
doc ───────┘ └─┘ └┘ ┴ ┴ └┘ └─┘
txt ───────┘ └─┘ └┘ ┴ ┴ └┘ └─┘
par ───────┘ └─┘ └┘ ┴ ┴ └┘ └─┘
pid ───────┘ └─┘ └┘ ┴ ┴ └┘ └┘┴
st ───────────────────────────────────────────────────────────┘└┘└
262 rw I.mem_leading_coeff_nth at this,
src └─┘ └──────┘
typ └─┘└─────────────────────┘└──────┘
doc └─┘ └──────┘
txt └─┘ └──────┘
par └─┘ └──────┘
pid ┴ └──────┘
st ─────────────────────────────────────┘└─
263 rcases this with ⟨q, hq, hdq, hlqp⟩,
id └──┘
src └─────┘ └──────────────────────┘
typ └─────┘└──┘└──────────────────────┘
doc └─────┘ └──────────────────────┘
txt └─────┘ └──────────────────────┘
par └─────┘ └──────────────────────┘
pid ┴ └──────────────────────┘
st ──────────────────────────────────────┘└─
264 have hq0 : q ≠ 0,
id ┴
src └─────────┘ ┴ └┘
typ └─────────┘┴┴ └┘
doc └─────────┘ ┴ └┘
txt └─────────┘ ┴ └┘
par └─────────┘ ┴ └┘
pid └──────┘└─┘ ┴ ┴┴
st ───────────────────┘└─
265 { intro H, rw [← polynomial.leading_coeff_eq_zero] at H,
id └──────────────────────────────┘
src └─────┘ └────┘└──────────────────────────────┘└────┘
typ └─────┘ └────┘└──────────────────────────────┘└────┘
doc └─────┘ └────┘ └────┘
txt └─────┘ └────┘ └────┘
par └─────┘ └────┘ └────┘
pid └┘ └──┘ ┴└───┘
st ─────┘└─────┘└──────────────────────────────────────┘┴└───┘└─
266 rw [hlqp, polynomial.leading_coeff_eq_zero] at H, exact hp0 H },
id └──┘ └──────────────────────────────┘ └─┘ ┴
src └──┘ └┘└──────────────────────────────┘└────┘ └────┘ ┴ ┴
typ └──┘└──┘└┘└──────────────────────────────┘└────┘ └────┘└─┘┴┴┴
doc └──┘ └┘ └────┘ └────┘ ┴ ┴
txt └──┘ └┘ └────┘ └────┘ ┴ ┴
par └──┘ └┘ └────┘ └────┘ ┴ ┴
pid └┘ └┘ ┴└───┘ ┴ ┴ ┴
st ─────────────┘└────────────────────────────────┘┴└───┘└────────────┘└┘└
267 have h1 : p.degree = (q * polynomial.X ^ (k - q.nat_degree)).degree,
id └──────┘ ┴ └──────────┘ ┴ ┴ ┴ └──────────┘
src └────────┘└──────┘┴ ┴ ┴┴┴└──────────┘┴┴┴ ┴┴┴└──────────┘└───────┘
typ └────────┘└──────┘┴ ┴ ┴┴┴└──────────┘┴┴┴ ┴┴┴┴└──────────┘└───────┘
doc └────────┘└──────┘┴ ┴ ┴ ┴└──────────┘┴ ┴ ┴ ┴└──────────┘└───────┘
txt └────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───────┘
par └────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───────┘
pid └─────┘└─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────┘┴
st ──────────────────────────────────────────────────────────────────────┘└─
268 { rw [polynomial.degree_mul_eq', polynomial.degree_X_pow],
id └───────────────────────┘ └─────────────────────┘
src └──┘└───────────────────────┘└┘└─────────────────────┘┴
typ └──┘└───────────────────────┘└┘└─────────────────────┘┴
doc └──┘ └┘ ┴
txt └──┘ └┘ ┴
par └──┘ └┘ ┴
pid └┘ └┘ ┴
st ─────┘└───────────────────────────┘└───────────────────────┘└──
269 rw [polynomial.degree_eq_nat_degree hp0, polynomial.degree_eq_nat_degree hq0],
id └─────────────────────────────┘ └─┘ └─────────────────────────────┘ └─┘
src └──┘└─────────────────────────────┘┴ └┘└─────────────────────────────┘┴ ┴
typ └──┘└─────────────────────────────┘┴└─┘└┘└─────────────────────────────┘┴└─┘┴
doc └──┘ ┴ └┘ ┴ ┴
txt └──┘ ┴ └┘ ┴ ┴
par └──┘ ┴ └┘ ┴ ┴
pid └┘ ┴ └┘ ┴ ┴
st ────────────────────────────────────────────┘└───────────────────────────────────┘└──
270 rw [← with_bot.coe_add, nat.add_sub_cancel', hn],
id └──────────────┘ └─────────────────┘ └┘
src └────┘└──────────────┘└┘└─────────────────┘└┘ ┴
typ └────┘└──────────────┘└┘└─────────────────┘└┘└┘┴
doc └────┘ └┘ └┘ ┴
txt └────┘ └┘ └┘ ┴
par └────┘ └┘ └┘ ┴
pid └──┘ └┘ └┘ ┴
st ───────────────────────────┘└───────────────────┘└──┘┴
271 { refine le_trans (polynomial.nat_degree_le_of_degree_le hdq) (le_of_lt h) },
st ┴
272 rw [polynomial.leading_coeff_X_pow, mul_one],
273 exact mt polynomial.leading_coeff_eq_zero.1 hq0 },
st ┴
274 have h2 : p.leading_coeff = (q * polynomial.X ^ (k - q.nat_degree)).leading_coeff,
275 { rw [← hlqp, polynomial.leading_coeff_mul_X_pow] },
src ┴
typ ┴
doc ┴
txt ┴
par ┴
pid ┴
st ┴ ┴
276 have := polynomial.degree_sub_lt h1 hp0 h2,
277 rw [polynomial.degree_eq_nat_degree hp0] at this,
278 rw ← sub_add_cancel p (q * polynomial.X ^ (k - q.nat_degree)),
279 refine (ideal.span ↑s).add_mem _ ((ideal.span ↑s).mul_mem_right _),
280 { by_cases hpq : p - q * polynomial.X ^ (k - q.nat_degree) = 0,
281 { rw hpq, exact ideal.zero_mem _ },
st ┴
282 refine ih _ _ (I.sub_mem hp (I.mul_mem_right hq)) rfl,
283 rwa [polynomial.degree_eq_nat_degree hpq, with_bot.coe_lt_coe, hn] at this },
st ┴
284 exact hs2 ⟨polynomial.mem_degree_le.2 hdq, hq⟩ }
st └─
285 end⟩⟩
st ──┘
286
287 theorem is_noetherian_ring_mv_polynomial_fin {n : ℕ} [is_noetherian_ring R] :
id ┴ └────────────────┘ ┴
src ┴ └────────────────┘
typ ┴ └────────────────┘ ┴
288 is_noetherian_ring (mv_polynomial (fin n) R) :=
id └────────────────┘ └───────────┘ └─┘ ┴ ┴
src └────────────────┘ └───────────┘ └─┘
typ └────────────────┘ └───────────┘ └─┘ ┴ ┴
doc └───────────┘
289 begin
st └─────
290 induction n with n ih,
id ┴
src └────────┘ └────────┘
typ └────────┘┴└────────┘
doc └────────┘ └────────┘
txt └────────┘ └────────┘
par └────────┘ └────────┘
pid ┴ ┴└───────┘
st ──────────────────────┘└─
291 { exact is_noetherian_ring_of_ring_equiv R
id └──────────────────────────────┘
src └────┘└──────────────────────────────┘┴ └
typ └────┘└──────────────────────────────┘┴ └
doc └────┘ ┴ └
txt └────┘ ┴ └
par └────┘ ┴ └
pid ┴ ┴ └
st ───┘└────────────────────────────────────────
292 ((mv_polynomial.pempty_ring_equiv R).symm.trans $ mv_polynomial.ring_equiv_of_equiv _
id └─────────────────────────────┘ ┴ └───────────────────────────────┘
src ─────┘ └─────────────────────────────┘┴ └───────────┘ ┴└───────────────────────────────┘└──
typ ─────┘ └─────────────────────────────┘┴┴└───────────┘ ┴└───────────────────────────────┘└──
doc ─────┘ └─────────────────────────────┘┴ └───────────┘ ┴└───────────────────────────────┘└──
txt ─────┘ ┴ └───────────┘ ┴ └──
par ─────┘ ┴ └───────────┘ ┴ └──
pid ─────┘ ┴ └───────────┘ ┴ └──
st ────────────────────────────────────────────────────────────────────────────────────────────
293 ⟨pempty.elim, fin.elim0, λ x, pempty.elim x, λ x, fin.elim0 x⟩) },
id └─────────┘ └───────┘
src ───────┘ └┘ └┘ └──┘└─────────┘┴ └┘ └──┘└───────┘┴ └─┘
typ ───────┘ └┘ └┘ └──┘└─────────┘┴ └┘ └──┘└───────┘┴ └─┘
doc ───────┘ └┘ └┘ └──┘ ┴ └┘ └──┘ ┴ └─┘
txt ───────┘ └┘ └┘ └──┘ ┴ └┘ └──┘ ┴ └─┘
par ───────┘ └┘ └┘ └──┘ ┴ └┘ └──┘ ┴ └─┘
pid ───────┘ └┘ └┘ └──┘ ┴ └┘ └──┘ ┴ └┘┴
st ───────────────────────────────────────────────────────────────────────┘└┘└
294 exact @is_noetherian_ring_of_ring_equiv (polynomial (mv_polynomial (fin n) R)) _
id └──────────────────────────────┘ └────────┘
src └────┘ └──────────────────────────────┘┴ └────────┘┴ ┴ ┴ └┘ └────
typ └────┘ └──────────────────────────────┘┴ └────────┘┴ ┴ ┴ └┘ └────
doc └────┘ ┴ └────────┘┴ ┴ ┴ └┘ └────
txt └────┘ ┴ ┴ ┴ ┴ └┘ └────
par └────┘ ┴ ┴ ┴ ┴ └┘ └────
pid ┴ ┴ ┴ ┴ ┴ └┘ └────
st ───────────────────────────────────────────────────────────────────────────────────
295 (mv_polynomial (fin (n+1)) R) _
id └───────────┘ ┴ ┴
src ───┘ └───────────┘┴ ┴ ┴└──┘ └───
typ ───┘ └───────────┘┴ ┴ ┴└──┘┴└───
doc ───┘ └───────────┘┴ ┴ └──┘ └───
txt ───┘ ┴ ┴ └──┘ └───
par ───┘ ┴ ┴ └──┘ └───
pid ───┘ ┴ ┴ └──┘ └───
st ────────────────────────────────────
296 ((mv_polynomial.option_equiv_left _ _).symm.trans (mv_polynomial.ring_equiv_of_equiv _
id └─────────────────────────────┘ └───────────────────────────────┘
src ───┘ └─────────────────────────────┘└───────────────┘ └───────────────────────────────┘└──
typ ───┘ └─────────────────────────────┘└───────────────┘ └───────────────────────────────┘└──
doc ───┘ └─────────────────────────────┘└───────────────┘ └───────────────────────────────┘└──
txt ───┘ └───────────────┘ └──
par ───┘ └───────────────┘ └──
pid ───┘ └───────────────┘ └──
st ───────────────────────────────────────────────────────────────────────────────────────────
297 ⟨λ x, option.rec_on x 0 fin.succ, λ x, fin.cases none some x,
src ─────┘ └──┘ ┴ └─┘ └┘ └──┘ ┴ ┴ ┴ └─
typ ─────┘ └──┘ ┴ └─┘ └┘ └──┘ ┴ ┴ ┴ └─
doc ─────┘ └──┘ ┴ └─┘ └┘ └──┘ ┴ ┴ ┴ └─
txt ─────┘ └──┘ ┴ └─┘ └┘ └──┘ ┴ ┴ ┴ └─
par ─────┘ └──┘ ┴ └─┘ └┘ └──┘ ┴ ┴ ┴ └─
pid ─────┘ └──┘ ┴ └─┘ └┘ └──┘ ┴ ┴ ┴ └─
st ────────────────────────────────────────────────────────────────────
298 by rintro ⟨none | x⟩; [refl, exact fin.cases_succ _],
id └────────────┘
src ─────┘ ┴└───────────────┘└─┘└──┘└──────┘└────────────┘└────
typ ─────┘ ┴└───────────────┘└─┘└──┘└──────┘└────────────┘└────
doc ─────┘ ┴└───────────────┘└─┘└──┘└──────┘ └────
txt ─────┘ ┴└───────────────┘└─┘└──┘└──────┘ └────
par ─────┘ ┴└───────────────┘└─┘└──┘└──────┘ └────
pid ─────┘ └───────────────────────────────┘ └────
st ───────┘└────────────────────────────────────────────────┘└─
299 λ x, fin.cases rfl (λ i, show (option.rec_on (fin.cases none some (fin.succ i) : option (fin n))
id └─┘ └───────────┘ └───────┘ └──┘ └──┘ └────┘ └─┘ ┴
src ─────┘ └──┘ ┴└─┘┴ └──┘ ┴ └───────────┘┴ └───────┘┴└──┘┴└──┘┴ ┴ └──┘└────┘┴ └─┘┴ └──
typ ─────┘ └──┘ ┴└─┘┴ └──┘ ┴ └───────────┘┴ └───────┘┴└──┘┴└──┘┴ ┴ └──┘└────┘┴ └─┘┴┴└──
doc ─────┘ └──┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └──
txt ─────┘ └──┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └──
par ─────┘ └──┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └──
pid ─────┘ └──┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └──
st ───────────────────────────────────────────────────────────────────────────────────────────────────────
300 0 fin.succ : fin n.succ) = _, by rw fin.cases_succ) x⟩))
id └──────┘ └────┘ ┴ └────────────┘
src ─────────┘└──────┘└─┘ ┴└────┘└┘┴└─────┘└─┘└────────────┘└┘ └───
typ ─────────┘└──────┘└─┘ ┴└────┘└┘┴└─────┘└─┘└────────────┘└┘ └───
doc ─────────┘ └─┘ ┴ └┘ └─────┘└─┘ └┘ └───
txt ─────────┘ └─┘ ┴ └┘ └─────┘└─┘ └┘ └───
par ─────────┘ └─┘ ┴ └┘ └─────┘└─┘ └┘ └───
pid ─────────┘ └─┘ ┴ └┘ └────────┘ └┘ └───
st ───────────────────────────────────────┘└────────────────┘└──────
301 (@@is_noetherian_ring_polynomial _ ih)
id └───────────────────────────┘ └┘
src ───┘ └───────────────────────────┘└─┘ └┘
typ ───┘ └───────────────────────────┘└─┘└┘└┘
doc ───┘ └───────────────────────────┘└─┘ └┘
txt ───┘ └─┘ └┘
par ───┘ └─┘ └┘
pid ───┘ └─┘ ┴┴
st ──────────────────────────────────────────┘
302 end
st └─┘
303
304 theorem is_noetherian_ring_mv_polynomial_of_fintype {σ : Type v} [fintype σ]
id └─────┘ ┴
src └─────┘
typ └─────┘ ┴
doc └─────┘
305 [is_noetherian_ring R] : is_noetherian_ring (mv_polynomial σ R) :=
id └────────────────┘ ┴ └────────────────┘ └───────────┘ ┴ ┴
src └────────────────┘ └────────────────┘ └───────────┘
typ └────────────────┘ ┴ └────────────────┘ └───────────┘ ┴ ┴
doc └───────────┘
306 trunc.induction_on (fintype.equiv_fin σ) $ λ e,
id └────────────────┘ └───────────────┘ ┴ ┴
src └────────────────┘ └───────────────┘
typ └────────────────┘ └───────────────┘ ┴ ┴
doc └───────────────┘
307 @is_noetherian_ring_of_ring_equiv (mv_polynomial (fin (fintype.card σ)) R) _ _ _
id └──────────────────────────────┘ └───────────┘ └─┘ └──────────┘ ┴ ┴
src └──────────────────────────────┘ └───────────┘ └─┘ └──────────┘
typ └──────────────────────────────┘ └───────────┘ └─┘ └──────────┘ ┴ ┴
doc └───────────┘ └──────────┘
308 (mv_polynomial.ring_equiv_of_equiv _ e.symm) is_noetherian_ring_mv_polynomial_fin
id └───────────────────────────────┘ ┴└───┘ └──────────────────────────────────┘
src └───────────────────────────────┘ └───┘ └──────────────────────────────────┘
typ └───────────────────────────────┘ ┴└───┘ └──────────────────────────────────┘
doc └───────────────────────────────┘